\documentclass{llncs} 

\usepackage{stmaryrd}
\usepackage{yhmath}
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{amsmath, amssymb}
\usepackage{upgreek}
\usepackage{mathrsfs}
\usepackage{multirow}
% \usepackage[all]{xy}


\usepackage{url}
\usepackage{macros}
           


\title{How many reversible CCS are there?}
\author{Ivan Lanese...} 
\institute{}

\date{}


\pagestyle{plain}

\begin{document}

\maketitle

\section{Introduction}
We want to study which are the choices in defining a reversible
variant of a given calculus. This will allow us to give a clear
structure to the state space of reversible calculi, and as a side
effect we will have for free some proofs of equivalence between
different variants of the same calculus. 

\section{Studying general reversibility}
We first want to study the properties of reversible calculi. Since we
are interested in reversibility in a concurrency scenario we will
consider causal consistency reversibility, as defined in
\cite{DanosK04}.  Intuitively, in causal consistent reversibility
actions are not reversed in the exact order of their forward
execution, but concurrent actions can be reversed in any order, while
causal dependencies should be respected, i.e., consequences should be
reverted before their causes.

In \cite{DanosK04} and subsequent works, three properties are
considered relevant for causal consistent reverisbility, and proved to
holds for RCCS. We will state them below, and require them to hold in
the calculi we consider. We start by introducing some notation.

We will consider two reversible calculi with processes (some calculi
distinguish processes and configurations, since we are at the high
level of abstraction we have no need to do this distinction) ranged
over by $R$ and $S$, respectively. We assume the calculi have a notion
of forward and backward reduction, denoted as $\fw$ and $\bk$
respectively, and a notion of barbs. We will write $R \barbop{a}$ to
say that $R$ has a (strong) barb at $a$. We will denote as $\fwt$ and
$\bkt$ the reflexive and transitive closures of $\fw$ and $\bk$,
respectively. We denote as $\red$ the union of $\fw$ and $\bk$, and as
$\redt$ its reflexive and transitive closure.

To define causal consistency we need a notion of equivalence between
traces. We use $t$ to range over transitions, and $\rev{t}$ to denote
an inverse transition of $t$. We denote with $\epsilon$ the empty
trace, and with $;$ the composition of traces. We also assume a notion
of concurrency between transitions. Given two concurrent transitions
$t_1$ and $t_2$ there are two transitions $t_2/t_1$ and $t_1/t_2$ such
that $t_1;t_2/t_1$ and $t_2;t_1/t_2$ are cofinal.

\begin{definition}
The causal consistency relation $\cc$ is the minimum relation satisfying:
$$t;\rev{t} \cc \epsilon \qquad t_1;t_2/t_1 \cc t_2;t_1/t_2 \textrm{ if } t_1,t_2 \textrm{ are concurrent}$$
\end{definition}

We can now formalize the properties for causal consistency.

\begin{property}[Loop Lemma]\label{prop:loop}
For each $R \fw R'$ we have $R' \bk R$ and vice versa.
\end{property}

\begin{property}[Parabolic Lemma]\label{prop:parabolic}
For each $R \redt R'$ there is $R''$ such that $R \bkt R'' \fwt R'$.
\end{property}

The parabolic lemma above is weaker than the one in the literature,
which also requires $R \redt R' \cc R \bkt R'' \fwt R'$. However the
parabolic lemma in the literature can be easily derived from the one
above and the causal consistency property below. Using our formulation
ensures that the two properties are less overlapping.

\begin{property}[Causal consistency]\label{prop:causal}
Two computations coinitial and cofinal are causal consistent.
\end{property}

The causal consistency theorem in the literature also has the other
direction, requiring that causal consistent configurations are
coinitial and cofinal, put this follows directly from the definition
of causal consistency.

The property below is not required/proved in \cite{DanosK04},
but it holds in RCCS.

Each process has a finite past.

\begin{property}[Finite past]\label{prop:finitepast}
There are no infinite backward computations. 
\end{property}

We want now to formalize the fact
that the two calculi are reversible variants of the same forward-only
calculus. We assume processes of the forward only calculus are ranged
over by $P$. 

We model the fact that the forward-only calculus is the basis of the
two reversible calculi by defining a function $\del$ mapping
processes of the reversible calculus into processes of the
forward-only calculus and forward transitions of the reversible
calculus to transitions of the forward-only calculus (this can be seen
as a functor among categories whose objectes are processes and arrows
are reductions). We assume $\del$ enjoys a few properties.

First, $\del$ is total.

\begin{property}\label{prop:gammatot}
Function $\del$ is total.
\end{property}

Second, $\del$ is functorial.

\begin{property}\label{prop:gammafun}
Let $R \fw R'$ a forward transition. Then $\del(R \fw R')=\del(R)
\red \del(R')$.
\end{property}

Third, $\del$ is barb preserving.

\begin{property}\label{prop:gammabarbs}
For each $R$, $R$ and $\del(R)$ have the same barbs.
\end{property}

Fourth, $\del$ can lift a process to a reversible process without
backward moves.

\begin{property}\label{prop:gammasurj}
For each $P$ there is an $R$ such that $\del(R)=P$ and $R$ has no
backward moves.
\end{property}

Fifth, $\del$ can lift transitions.

\begin{property}\label{prop:gammaliftred}
If $P \red P'$ and $\del(R)=P$ then there exists $R \fw R'$ with
$\del(R')=P'$.
\end{property}

Sixth, $\del$ should preserve the concurrency structure of the
calculus.

\begin{property}\label{prop:gammaconc}
$R \fw R_1$ and $R \fw R_2$ are concurrent iff $\del(R \fw R_1)$ and $\del(R \fw R_2)$ are concurrent. 
\end{property}

We start by proving that in a calculus satisfying
properties~\ref{prop:loop}, \ref{prop:parabolic} and
\ref{prop:finitepast} each process has a unique oldest ancestor. If
$R$ is the name of the process than we call $R_{\bot}$ its oldest
ancestor.

\begin{lemma}\label{lemma:uniqueRbot}
Take a calculus satisfying properties ~\ref{prop:loop},
\ref{prop:parabolic} and \ref{prop:finitepast}.  Given a process $R$
there exists a unique process $R_{\bot}$ such that $R$ goes backward
to $R_{\bot}$ and $R_{\bot}$ has no backward transitions.
\end{lemma}
\begin{proof}
For the existence, take $R$ and go backward. Since there are no
infinite backward computations (property~\ref{prop:finitepast}) then
we reach one such $R_{\bot}$.

For the uniqueness, assume towards a contradiction that both
$R^1_{\bot}$ and $R^2_{\bot}$ satisfy the thesis. Because of the loop
lemma (property~\ref{prop:loop}) we have a computation from
$R^1_{\bot}$ to $R$, thus we also have a computation from $R^1_{\bot}$
to $R^2_{\bot}$. Because of the parabolic lemma
(property~\ref{prop:parabolic}), the computation can be written as
composition of a backward part followed by a forward part. However the
backward part should be empty, since $R^1_{\bot}$ has no backward
reduction. Thus the computation is forward, and by loop lemma there is
a backward computation from $R^2_{\bot}$ to $R^1_{\bot}$. This is
however impossible since $R^2_{\bot}$ has no backward reduction. This
proves the uniqueness.
\end{proof}

A property that follows from causal consistency is that each reduction
$t$ has at most one inverse $\rev{t}$ (actually exactly one, thanks to
the Loop lemma).

\begin{lemma}\label{lemma:uniquecomp}
Given a transition $t$ there is at most one transition
$\rev{t}$.
\end{lemma}
\begin{proof}
Assume that there are two such transitions. The two corresponding one
transition computations are coinitial and cofinal, thus they should be
causally equivalent. However no axiom can be applied to them. Since
this is an absurd the thesis follows.
\end{proof}

We now show that two processes with no backward transitions
corresponding to the same forward process are equivalent.

\begin{lemma}\label{lemma:botequiv}
If $\del(R^1_{\bot})=\del(R^2_{\bot})$ then $R^1_{\bot}$ and
$R^2_{\bot}$ are strong backward and forward barbed equivalent.
\end{lemma}
\begin{proof}
Let us define the relation $\rcal$ as follows.
$R^1_{\bot} \rcal R^2_{\bot}$ iff $\del(R^1_{\bot})=\del(R^2_{\bot})$.
If $R \rcal R'$, $R \fw R_1$, $R' \fw
R'_1$ and $\del(R_1)=\del(R'_1)$ then $R_1 \rcal R'_1$.
We show that $\rcal$ is a strong backward and forward barbed equivalence.

Before starting we show a few properties  of $\rcal$ that we will use
during the proof.

The first property is that $R \rcal R'$ implies $\del(R)=\del(R')$
(while the opposite may not be true). The property follows by
definition.

The second property is that $R \rcal R'$ implies $R_{\bot} \rcal
R'_{\bot}$. The derivation of $R \rcal R'$ is based on two
computations of the same length (possibly $0$) $R''_{\bot} \fwt R$ and
$R'''_{\bot} \fwt R'$ with $R''_{\bot} \rcal R'''_{\bot}$. However
from Lemma~\ref{lemma:uniqueRbot} we have $R''_{\bot}=R_{\bot}$ and
$R'''_{\bot}=R'_{\bot}$, thus $R_{\bot} \rcal R'_{\bot}$.

Now we can go into the barbed equivalence proof.

The condition on barbs follows by property~\ref{prop:gammabarbs}.

Assume now $R \rcal R'$ and $R \fw R_1$. Thanks to
property~\ref{prop:gammafun} we have $\del(R \fw R_1)=\del(R) \red
\del(R_1)$.  As shown before $R \rcal R'$ implies
$\del(R)=\del(R')$. Then by property~\ref{prop:gammaliftred} we have
that there exists $R' \fw R'_1$ such that $\del(R'_1) =\del(R_1)$. Then, by definition of $\rcal$, $R' \rcal R'_1$.

Assume now $R \rcal R'$ and $R \bk R_1$. Let us consider
$R_\bot$. Consider the computation $R_\bot \fwt R$ ensuring $R \rcal
R'$.  From the parabolic lemma since $R_\bot \fwt R \bk R_1$ we have a
computation $R_\bot \fwt R_1$ (note in fact that the backward part of
the computation should be empty). From the causal consistency lemma
the two computations $R_\bot \fwt R_1$ and $R_\bot \fwt R \bk R_1$
differ only for commuting concurrent actions and simplifying reverse
actions. In particular, the only way to remove the backward action $R
\bk R_1$ is to simplify it with a forward action in $R_\bot \fwt R$,
and this requires that it commutes with all the actions after it.
From lemma~\ref{lemma:uniquecomp} there is only one possible choice.
Commute this reduction with all the following reductions, to make it
the last one. This allows to get a computation $R_\bot \fwt R_1 \fw R$.

Let us move to the other side. Consider the computation $R'_\bot \fwt
R'$ ensuring $R \rcal R'$. The same kind of commutations done above
can be done in this computation, since commuting squares are preserved
and reflected by $\del$ thanks to property~\ref{prop:gammaconc}. Thus
we get a computation of the form $R'_\bot \fwt R'_1 \fw R'$
corresponding to the one above, ensuring that $R_1 \rcal R'_1$. Since
by loop lemma $R' \bk R'_1$ we have the thesis.
\end{proof}

\begin{theorem}\label{th:main}
If all the hypothesis are satisfied, then the two calculi are strong
backward and forward barbed equivalent.
\end{theorem}
\begin{proof}
We have to show that for each process in one calculus there is a
strong backward and forward barbed equivalent one in the other
calculus. Take a process $R$ and consider $R_\bot$. Consider
$\del(R_\bot)$. Thanks to property~\ref{prop:gammasurj} there is an
$S$ such that $\del(S)=\del(R_\bot)$ and $S$ has no backward moves.
Let us call it $S_\bot$. From Lemma~\ref{lemma:botequiv} $R_\bot$ and
$S_\bot$ are strong backward and forward barbed equivalent. In
particular, since $R_\bot \fwt R$ there is a process $S$ such that
$S_\bot \fwt S$ and $R$ and $S$ are strong backward and forward barbed
equivalent.
\end{proof}

\section{Equivalence results}
In this section we use the theory developed above to prove
equivalences among reversible calculi defined in various ways.

The first such calculus is RCCS from~\cite{DanosK04}. 

\begin{lemma}\label{lemma:propRCCS}
All the properties above hold for RCCS (restricted to coherent
processes), and for its projection to CCS defined on transitions by
removing all the additional information and on states by removing all
history information.
\end{lemma}
\begin{proof}
Property \ref{prop:loop} is proved in \cite[Lemma
  6]{DanosK04}. Property~\ref{prop:parabolic} is proved in \cite[Lemma
  10]{DanosK04}. Property~\ref{prop:causal} is proved in
\cite[Th. 1]{DanosK04}. Property~\ref{prop:finitepast} is easily
proved by noticing that each backward step decreases the amount of
history information. Properties~\ref{prop:gammatot},
\ref{prop:gammafun} and \ref{prop:gammabarbs} follows by definition of
$\del$.  Property~\ref{prop:gammasurj} is proved in
\cite[Sec. 2.2]{DanosK04}. Property~\ref{prop:gammaliftred} is proved
in \cite[Lemma 4]{DanosK04}. Property~\ref{prop:gammaconc} follows from
the definition of $\del$.
\end{proof}

As second calculus we consider $\rpi$~\cite{RHOPI}. However, $\rpi$ is
a reversible version of HOpi, not of CCS, and it is asynchronous. It
is easy however to define a reversible version of CCS using the same
technique, and we do it in Appendix~\ref{app:rCCS}. We will call it
$\rCCS$. 

\begin{lemma}\label{lemma:proprhoCCS}
All the properties above hold for $\rCCS$ (restricted to consistent
configurations), and for its projection to CCS defined on transitions
by considering the CCS transition involving the same prefixes and on
states by removing all history information.
\end{lemma}
\begin{proof}
Property \ref{prop:loop} can easily be adapted from \cite[Lemma
  5]{RHOPI}.  Property~\ref{prop:parabolic} can easily be adapted from
\cite[Lemma 8]{RHOPI}. Property~\ref{prop:causal} can easily be
adapted from \cite[Th. 1]{RHOPI}.  Property~\ref{prop:finitepast} is
easily proved by noticing that each backward step decreases the amount
of history information.  Property~\ref{prop:gammatot} follows by
definition of $\gamma$.  Property~\ref{prop:gammafun} can easily be
adapted from \cite[Lemma 4]{RHOPI}.  Property \ref{prop:gammabarbs}
follows by definition of $\del$.  Property~\ref{prop:gammasurj} can
easily be proved by labeling each thread with a distinct key.
Property~\ref{prop:gammaliftred} can easily be proved by induction on
the derivation of the transition.  Property~\ref{prop:gammaconc}
follows from the definition of $\del$.
\end{proof}

As third calculus we consider CCSk, as defined in~\cite{PhillipsU07}.

\begin{lemma}\label{lemma:propCCSk}
All the properties above hold for CCSk (restricted to reachable
configurations), and for its projection to CCS defined on transitions
by considering the CCS transition involving the same prefixes and on
states by taking only the standard part of processes.
\end{lemma}
\begin{proof}
Property \ref{prop:loop} is proved in \cite[Prop. 1]{PhillipsU07}.
Property~\ref{prop:parabolic} is proved in \cite[Lemma 5.12]{PhillipsU07}. 
Property~\ref{prop:causal} follows from \cite[Lemmas 5.14,5.18]{PhillipsU07}.
Property~\ref{prop:finitepast} is easily proved
by noticing that each backward step decreases the non standard part of
processes.  Property~\ref{prop:gammatot} follows by definition of
$\gamma$.  Property~\ref{prop:gammafun} is proved in
\cite[Th. 5.21]{PhillipsU07}.  Property \ref{prop:gammabarbs} follows
by definition of $\del$.  Property~\ref{prop:gammasurj} is trivial,
since normal processes are a subset of reversible processes, and they
do not have backward actions. Property~\ref{prop:gammaliftred} is
proved in \cite[Th. 5.21]{PhillipsU07}.  Property~\ref{prop:gammaconc}
follows from the definition of $\del$.
\end{proof}

As a straightforward corollary of Theorem~\ref{th:main} and
lemmas~\ref{lemma:propRCCS}, \ref{lemma:proprhoCCS} and
\ref{lemma:propCCSk} we get:

\begin{corollary}
RCCS, $\rCCS$ and CCSk are strong forward and backward bisimilar.
\end{corollary}

\section{Removing properties}
In this section we show that if we remove one of the conditions above,
we will prove equivalences between RCCS and a non strong backward and
forward barbed congruent calculus, thus reaching an absurd. In other
words, all the conditions are needed for our result.

\paragraph{Property~\ref{prop:loop}.}
We get RCCS with irreversible actions, as described
in~\cite{DanosK05}.  Let us show that all the other properties
hold. This is trivial for properties \ref{prop:finitepast},
\ref{prop:gammatot}, \ref{prop:gammafun}, \ref{prop:gammabarbs},
\ref{prop:gammasurj}, \ref{prop:gammaliftred} and
\ref{prop:gammaconc}. 

Let us prove property~\ref{prop:parabolic}. Consider the same
computation in RCCS. Since the parabolic lemma holds in RCCS we can
find a computation of the desired form in RCCS. This is a valid
computation in RCCS with irreversible actions only if no backward move
corresponds to an irreversible action. Take one such backward
move. Either it was available in the original computation, and in this
case the thesis follows, or it has been introduced together with its
complement. In this last case both the action and the inverse can be
removed. Thus the thesis follows.

Let us prove property~\ref{prop:causal}. Let us take two coinitial and
cofinal computation. The same computations are coinitial and cofinal
in RCCS, and thus are causal equivalent there. Concurrent actions are
the same. Also, two inverse transitions can always be removed also in
RCCS with irreversible actions, thus the thesis follows. Notice that
there is no need of introducing a pair of actions, since in case they
can be removed on the other side.

\paragraph{Property~\ref{prop:parabolic}.}
Given the properties~\ref{prop:loop} (Loop lemma)
and~\ref{prop:finitepast} (Finite past) then
Property~\ref{prop:parabolic} is actually equivalent to the uniqueness
of $R_\bot$. One implication is given by Lemma~\ref{lemma:uniqueRbot}.
We prove the other implication below.

\begin{lemma}\label{lemma:parab}
If in a calculus satisfying properties~\ref{prop:loop} and
\ref{prop:finitepast} for each $R$ there is a unique $R_\bot$ then
property~\ref{prop:parabolic} holds.
\end{lemma}
\begin{proof}
We do the proof for a given computation, by induction on the number
$n$ of backward transitions in the computation which are not at the
beginning. If $n=0$ then nothing has to be proved. Otherwise, take the
first backward transition $R \bk R'$ not at the beginning. Thus the
computation has the form $R^s \bkt R^0 \fwt R \bk R' \redt R''$. Since
$R$ goes back to both $R^0$ and $R'$ we have
$R^0_{\bot}=R'_{\bot}$. Thus $R^0 \bkt R^0_{\bot} \fwt R' \redt R''$
which has one less backward reduction not at the beginning.
The thesis follows by induction.
\end{proof}

Using the result above we can show that a variant of $\rCCS$ with
multiple memories with the same memory keys (what is not allowed by
$\rCCS$ well formedness rules) satisfies all the properties but the
Parabolic lemma.

It is clear that properties \ref{prop:loop}, \ref{prop:gammatot},
\ref{prop:gammafun}, \ref{prop:gammabarbs}, \ref{prop:gammasurj},
\ref{prop:gammaliftred}, \ref{prop:gammaconc} hold. Property
\ref{prop:finitepast} holds if the number of memories is finite, what
we can assume.

We have to prove property~\ref{prop:causal}. Let us take two
computations. Observe that two memories with the same keys are
exclusive, in the sense that if I use one of them to reverse a
computation I will never be able to reverse the other. In particular,
different choices on which memories to reverse cannot lead to the same
state. Thus in a pair of computations coinitial and cofinal the
choices must agree. Then the computations will not change by removing
the non-chosen memories. But these are two computations of $\rCCS$,
thus they are causally equivalent, and they are causally equivalent
for the same reasons in the calculus with multiple memories.

\paragraph{Property~\ref{prop:causal}.}
We give below two corollaries of causal consistency:

\begin{lemma}
If a calculus is causal consistent then two transitions coinitial
which are not concurrent lead to two disjoint sets of states unless
the initial transition is undone.
\end{lemma}
\begin{proof}
Assume there is a common state. Then we have two coinitial and cofinal
computations. Thanks to causal consistency, the two computations
should be causal consistent. Thus we should be able to transform the
first computation into the second using the causal consistency
axioms. Let us consider the first pair: we cannot apply the concurrent
diamond, then we have to apply the other axiom, i.e. undo one of the
actions. The thesis follows.
\end{proof}

The second corollary requires also the parabolic lemma.

\begin{lemma}
If a calculus is causal consistent and the parabolic lemma holds then
any backward reduction commutes with all the forward reductions before
it, unless one of them is its inverse.
\end{lemma}
\begin{proof}
Take a computation of the form $R \fwt R' \bk R''$. Thanks to the
parabolic lemma we also have a computation $R \bkt R_0 \fwt
R''$. Since the two computations are coinitial and cofinal they should
be equal up to causal equivalence. Thus the reduction $R' \bk R''$
should either disappear, and the only possibility is that it moves
near to its inverse, or commute with all the forward transitions. This
proves the thesis.
\end{proof}

Here we get a variant of RCCS similar to Laneve and Cardelli weak
coherent calculus in~\cite{CardelliL11}. Take $\rCCS$ and assume that
keys generated in forward computations are not fresh, but that the
same key can label only continuations of communications on the same
channel. I.e., continuations of communication on $a$ are labelled by
$k_a$, $k'_a$, \dots

We have the following computation below:

\begin{multline*}
k:\co{a}.P \parop k':a.Q \parop k'':\co{a}.P' \parop k''':a.Q' \fw\\
[k:\co{a}.P \parop k':a.Q;k_a;k'_a] \parop k_a:P \parop k'_a:Q \parop k'':\co{a}.P' \parop k''':a.Q' \fw\\
[k:\co{a}.P \parop k':a.Q;k_a;k'_a] \parop k_a:P \parop k'_a:Q \parop [k'':\co{a}.P' \parop k''':a.Q';k_a;k'_a] k_a:P' \parop k'_a:Q' \bk\\
k:\co{a}.P \parop k':a.Q \parop k'_a:Q \parop [k'':\co{a}.P' \parop k''':a.Q';k_a;k'_a] k_a:P'
\end{multline*}

The backward step is not the inverse of its predecessors, neither
concurrent to them. Thus this calculus is not causally consistent.  It
is easy to see that it satisfies property~\ref{prop:loop},
\ref{prop:finitepast}, and that it can be projected into CCS without
sum by a function $\del$ satisfying properties \ref{prop:gammatot},
\ref{prop:gammafun}, \ref{prop:gammabarbs}, \ref{prop:gammasurj},
\ref{prop:gammaliftred} and \ref{prop:gammaconc}. We only need to show
the property \ref{prop:parabolic} (Parabolic).

Thanks to Lemma~\ref{lemma:parab} we can equivalently prove that each
$R$ has a unique $R_{\bot}$. One can easily see that memories with the
same keys attach the same prefix to processes, thus rearranging them
will not change the processes obtained by undoing all the steps.

\paragraph{Property~\ref{prop:finitepast}.}
Here we may imagine to extend RCCS with infinite histories (the
business of representing them in a finite way is not particularly
relevant, since we do not assume any syntax for our calculi).

\paragraph{Property~\ref{prop:gammatot}.}
Here we get a reversible calculus with more states. Take RCCS and add
to it a state $\dagger$ with no transitions and no barbs. Make $\del$
not defined on $\dagger$. It is easy to see that properties
\ref{prop:loop}, \ref{prop:parabolic}, \ref{prop:causal},
\ref{prop:finitepast}, \ref{prop:gammafun}, \ref{prop:gammabarbs},
\ref{prop:gammasurj}, \ref{prop:gammaliftred} and \ref{prop:gammaconc}
hold.

\paragraph{Property~\ref{prop:gammafun}.}
Let us take as reversible calculus a CCS with determinstic
rollback. Note that in CCS for each pair of concurrent actions there
is an analogous pair of actions which are in interleaving (just take
the concurrent terms and apply the expansion law). Define $\del$ that
maps each reduction to its interleaving counterpart. Define instead
$\del$ on states as before. It is easy to see that in this setting
properties \ref{prop:loop}, \ref{prop:parabolic}, \ref{prop:causal},
\ref{prop:finitepast}, \ref{prop:gammabarbs}, \ref{prop:gammasurj},
\ref{prop:gammaliftred} and \ref{prop:gammaconc} hold.

\paragraph{Property~\ref{prop:gammabarbs}.}
It is easy to show that two RCCS calculi with different sets of names
(of the same cardinality) has made equivalent by our results if the
property~\ref{prop:gammabarbs} is removed by the premises. In fact,
take a bijective renaming among the two sets of names. Processes equal
up to this renaming will be confused, and they satisfy all the other
properties.

While this is the simplest example, many more calculi will get mixed,
since barbs are the main observable. E.g. all the reversible calculi
without concurrency and where in each state both a forward and a
backward transition are enabled become equivalent.

\paragraph{Property~\ref{prop:gammasurj}.}
Here we require that the reversible calculus has at least the states
of the forward one, as states with no history. Let us see first what happens by dropping the first requirement.

Let us take a reversible calculus with only process $\nil$, and as
normal calculus CCS, with $\del$ mapping $\nil$ to $\nil$.  It is easy
to see that this calculus respects properties \ref{prop:loop},
\ref{prop:parabolic}, \ref{prop:causal}, \ref{prop:finitepast},
\ref{prop:gammatot}, \ref{prop:gammafun}, \ref{prop:gammabarbs},
\ref{prop:gammaliftred} and \ref{prop:gammaconc} hold.

Let us see now what happens by dropping the second requirement.  Take
as reversible calculus all the RCCS processes obtained from a given
process with no backward reduction, and with basic calculus all the
projections of the processes above. It is easy to see that such a
calculus satisfies properties \ref{prop:loop}, \ref{prop:parabolic},
\ref{prop:causal}, \ref{prop:finitepast}, \ref{prop:gammatot},
\ref{prop:gammafun}, \ref{prop:gammabarbs}, \ref{prop:gammaliftred}
and \ref{prop:gammaconc} hold. However this calculus is different from
the subset of RCCS containing all the processes obtained from
computations of the lift of the CCS processes above, since in this
second calculus there are many processes with no backward reductions,
not equivalent.

\paragraph{Property~\ref{prop:gammaliftred}.}
Here we get a calculus where some forward transitions (and their
corresponding forward transitions) do not work, which is clearly not
strong backward and forward barbed equivalent.

Take RCCS, and assume communications on a given channel $a$ are not
allowed. In practice, the calculus has the same semantics of RCCS
where inputs and outputs on $a$ are replaced by $\nil$, but
different barbs. If we drop property~\ref{prop:gammaliftred} from the
preconditions of our theorem, we could use it to prove that this
calculus is equivalent to RCCS, while it is not since it has different
forward transitions. We just have to show that all the other
properties are satisfied. Properties \ref{prop:loop},
\ref{prop:parabolic}, \ref{prop:causal} and \ref{prop:finitepast},
are satisfied since they are in RCCS where all
communications on $a$ are replaced by $\nil$. Properties
\ref{prop:gammatot}, \ref{prop:gammafun} and \ref{prop:gammaconc} are
satisfied since the reversible calculus has less transitions. Property
\ref{prop:gammabarbs} and \ref{prop:gammasurj} are satisfied since the
calculus has the same states as RCCS.

\paragraph{Property~\ref{prop:gammaconc}.}
Assume that $\del$ projects any pair of concurrent actions into
concurrent actions, but does not lift pairs of concurrent actions. In
words, the reversible calculus may have less concurrent actions. For
simplicity consider CCS, transform all the pairs of concurrent actions
into interleaving using the expansion law, and consider its RCCS
semantics. The obtained calculus is different from RCCS, since
reductions cannot be undone out-of-order. It is however trivial to see
that properties \ref{prop:loop}, \ref{prop:parabolic},
\ref{prop:causal}, \ref{prop:finitepast}, \ref{prop:gammatot},
\ref{prop:gammafun}, \ref{prop:gammabarbs}, \ref{prop:gammasurj},
\ref{prop:gammaliftred} hold.

Note that the calculus above corresponds to sequential rollback, where
the last action is undone.

\section{Conclusions}
We can summarize the results of this paper by giving a comparison of
the calculi in the literature based on which properties they satisfy
and on their underlying calculus. In the table, RCCS + IA stands for
RCCS with irreversible actions, wc Rev Stru stands for weak coherent
reversible structures, co Rev Stru stands for coherent reversible
structures, CCS- stands for a subset of CCS, r$\mu$Oz stands for
reversible $\mu$ Oz. SPF stands for calculi whose SOS formalization is
in the simple path format~\cite{PhillipsU07}, and rSPF for their
reversible cariants. CCSk is just the instance of the general
framework to CCS.

Let us comment on why some properties are not verified in some
calculi. For RCCS + IA, irreversible actions make the Loop lemma to
fail. For reversible $\mu$Oz, spurious reductions are added to ensure
reversibility, thus the correspondance is a weak backward and forward
bisimulation. For weak coherent reversible structures the
impossibility to distinguish similar atoms make causal consistence to
fail. The property is reobtained by restricting the attention to
coherent reversible structures.

\begin{table}[t]
\begin{minipage}{\textwidth}
\begin{tabular}{|c||c|c|c|c|c|c|c|c|c|c|c|
}
\hline
& \multicolumn{10}{|c|}{Property}  & Underlying\\
& 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & calculus\\
\hline
\hline
RCCS \cite{DanosK04} & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & CCS\\
\hline
RCCS + IA \cite{DanosK05} & X & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & CCS\\
\hline 
$\rpi$ \cite{RHOPI} & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & HO$\pi$\\
\hline
r$\mu$Oz \cite{LienhardtLMS12} & \tick & \tick & \tick & \tick & \tick & X & \tick & \tick & X & \tick & $\mu$Oz\\
\hline
wc Rev Stru \cite{CardelliL11} & \tick & \tick & X & \tick & \tick & \tick & \tick & \tick & \tick & \tick & CCS- \\
\hline
co Rev Stru \cite{CardelliL11} & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & CCS-\\
\hline
rSPF \cite{PhillipsU07} & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & \tick & SPF\\
\hline
\end{tabular}
\end{minipage}
\caption{Properties of reversible calculi.} \label{table:calculi}
\end{table}



\bibliographystyle{plain} 
\bibliography{rhopi}



\appendix

\section{$\rCCS$}\label{app:rCCS}

We assume a $\names$ for CCS \emph{names}, and a set $\keys$ of
\emph{keys} for tracking causality information.. The set $\ids =
\names \cup \keys$ is called the set of \emph{identifiers}.  We let
(together with their decorated variants): $a,b,c$ range over $\names$;
$h,k,l$ range over $\keys$; $u,v,w$ range over $\ids$.

The syntax of $\rCCS$ is given in Figure~\ref{fig.syntax}.
\emph{Processes} of $\rCCS$, given by the $P,Q$
productions in Figure~\ref{fig.syntax}, are the standard processes of
CCS.

\myfig{
\begin{align*}
	 P,Q  &\syntaxdef \; \nil \ou \new{a}{P} \ou (P \parop Q) \ou \sum_i \alpha_i.P_i \\
         \alpha &\syntaxdef \; \co{a} \ou a\\
	 M,N  &\syntaxdef \; \nil \ou \new{u}{M}  \ou  (M \parop N) \ou \kappa : P \ou [\mu;k_1;k_2] \\
	 \kappa  &\syntaxdef \; k \ou \angbrk{h,\vect{h}}\cdot k \\
         \mu & \syntaxdef \;  ((\kappa_1:\co{a} + \sum_i \alpha_i.P_i) \parop (\kappa_2:a + \sum_j \alpha_j.P_j) \\
	& u \in \ids\; \; \;  a \in \names \; \; \;  h,k \in \keys\; \;\;  \kappa \in \tags
\end{align*}}
{Syntax of $\rCCS$}
{fig.syntax}


Processes in $\rCCS$ cannot directly execute, only \emph{configurations} can. 
\emph{Configurations} in $\rCCS$ are given by the $M,N$ productions in Figure~\ref{fig.syntax}.
A configuration is built up from \emph{threads} and \emph{memories}.

A \emph{thread} $\kappa:P$ is just a tagged process $P$, where the tag
$\kappa$ is either a single key $k$ or a pair of the form
$\angbrk{h,\vect{h}}\cdot k$, where $\vect{h}$ is a set of keys, with
$h \in \vect{h}$.  A tag serves as an identifier for a process.

A \emph{memory} is a process of the form $[\mu;k_1;k_2]$
which keeps track of the
fact that an input on $\kappa_1$ and an output on $\kappa_2$
interacted on channel $a$ producing continuations on $k_1$ and $k_2$. 

We note $\procs$ the set of $\rCCS$ processes, and $\confs$ the set of
$\rCCS$ configurations.  We call \emph{agent} an element of the set
$\agents = \procs \cup \confs$.  We let (together with their decorated
variants) $P,Q, R$ range over $\procs$; $L,M,N$ range over $\confs$;
and $A,B,C$ range over agents.  We call \emph{primitive thread
  process} a choice. We let
$\tau$ and its decorated variants range over primitive thread
processes.

Notions of free identifiers in $\rCCS$ are
classical.

The operational semantics of the $\rCCS$ calculus is defined via a
reduction relation $\red$, which is a binary relation over closed
configurations, and a structural congruence relation $\equiv$, which
is a binary relation over processes and configurations.  We define
evaluation contexts as ``configurations with a hole $\hole$'' given by
the following grammar:
$$\ectx \syntaxdef \hole \ou (M \parop \ectx) \ou \new{u}{\ectx}$$
General contexts $\cctx$ are just processes or configurations with a hole.
A congruence on processes and configurations is an equivalence relation $\rcal$ that is closed for general contexts:
$P \, \rcal \, Q \implies \cctx[P] \, \rcal \, \cctx[Q]$ and 
$M \, \rcal \, N \implies \cctx[M] \, \rcal \, \cctx[N]$.

\myfig{
\begin{mathpar}
	\inferrule*[left=(E.ParC)]{}
	{A \parop B \equiv B \parop A}
	\and
	\inferrule*[left=(E.ParA)]{}
	{A \parop (B \parop C) \equiv (A \parop B) \parop C}
	\and
	\inferrule*[left=(E.NilM)]{}
	{A \parop \nil \equiv A}
	\and
	\inferrule*[left=(E.NewN)]{}
	{\new{u}{\nil} \equiv \nil }
	\and
	\inferrule*[left=(E.NewC)]{}
	{\new{u}{\new{v}{A}} \equiv \new{v}{\new{u}{A}}}	
	\and
	\inferrule*[left=(E.NewP)]{}
	{(\new{u}{A}) \parop B \equiv \new{u}{(A \parop B)}}
	\and
	\inferrule*[left=(E.$\alpha$)]{}
	{A =_{\alpha} B \implies A \equiv B}
	\and
	\inferrule*[left=(E.TagN)]{}
	{\kappa: \new{a}{P} \equiv \new{a} \kappa: P }
	\and
	\inferrule*[left=(E.TagP)]{}
	{k: \prod_{i= 1}^{n} \tau_i \equiv \newop{\vect{h}}\prod_{i=1}^{n} (\angbrk{h_i,\vect{h}}\cdot k: \tau_i) \; \; \; \vect{h} = \rset{h_1,\ldots,h_n}}
\end{mathpar}
}
{Structural congruence for $\rpi$}
{fig.equiv}

The relation $\equiv$ is defined as the smallest congruence on
processes and configurations that satisfies the rules in
Figure~\ref{fig.equiv}. We note $t =_{\alpha} t'$ when terms $t,t'$
are equal modulo $\alpha$-conversion. In rule \textsc{E.TagP},
processes $\tau_i$ are primitive thread processes.  The structural
congruence rules are the usual rules for the CCS
(\textsc{E.ParC} to \textsc{E.$\alpha$}) without the rule dealing with
replication, and with the addition of two new rules dealing with tags:
\textsc{E.TagN} and \textsc{E.TagP}. Rule \textsc{E.TagN} is a scope
extrusion rule to push restrictions to the top level.  Rule
\textsc{E.TagP} allows to generate unique tags for each primitive
thread process in a configuration.

We say that a binary relation $\rcal$ on closed configurations is
\emph{evaluation-closed} if it satisfies the inference rules:
\begin{mathpar}
		\inferrule*[left=(R.Ctx)]{M\; \rcal \; N}
		{\ectx[M] \; \rcal \; \ectx[N]}	
		\and
		\inferrule*[left=(R.Eqv)]{M \equiv M' \\
		M' \; \rcal \; N' \\
		N' \equiv N}
		{M \; \rcal \; N}
\end{mathpar}
Relations $\fw$ and $\bk$ are defined
to be the smallest evaluation-closed binary relations on closed configurations satisfying the rules in Figure~\ref{fig.reduction}.

\myfig{
\begin{mathpar}
	\inferrule*[left=(R.Fw)\;\;]{}
	{(\kappa_1:\co{a}.P_1+Q_1) \parop (\kappa_2:a.P_2+Q_2) \fw \new{k_1,k_2}{(k_1:P) \parop (k_2:Q) \parop [(\kappa_1:\co{a}.P_1+Q_1) \parop (\kappa_2:a.P_2+Q_2);k_1;k_2]}}
	
	\and
	
	\inferrule*[left=(R.Bw)\;\;]{}
	{(k_1:P) \parop (k_2:Q) \parop [\mu;k_1;k_2] \bk \mu}
\end{mathpar}

}
{Reduction rules for $\rCCS$}{fig.reduction}

The rule for forward reduction (\textsc{R.Fw}) is the standard
communication rule of CCS with two side effects: (i) the creation of a
new memory to record the reduction; (ii) the tagging of the
continuations with the fresh keys $k_1$ and $k_2$.  The rule for
backward reduction (\textsc{R.Bw}) states that in presence of threads
tagged with keys $k_1$ and $k_2$, a memory
$[\mu;k_1;k_2]$ reinstates the
configuration $\mu$ that gave rise to the tagged threads.



\end{document}


